$\forall$${\it es}$:event\_system\{i:l\}, $l$:IdLnk, ${\it tg}$:Id, $e$:es{-}E(${\it es}$).
\\[0ex]($\uparrow$es{-}isrcv(${\it es}$; $e$))
\\[0ex]$\Rightarrow$ (es{-}lnk(${\it es}$; $e$) = $l$)
\\[0ex]$\Rightarrow$ (es{-}tag(${\it es}$; $e$) = ${\it tg}$)
\\[0ex]$\Rightarrow$ (es{-}kind(${\it es}$; $e$) = rcv($l$,${\it tg}$) $\in$ Knd)